#ifndef SAT_PROBLEM_H
#define SAT_PROBLEM_H

#include <vector>
#include <map>
#include <set>
#include <algorithm> 
#include <climits>
#include <cassert>
#include <ostream>

/// A Variable is represented by an int. Variables
/// start from 1 onwards. In a clause, a negative 
/// value of a Variable such as (-3), means 
/// not (Variable 3), while (+3) means (Variable 3). 

typedef int Variable; 

class Clause {
    typedef std::vector<Variable> Variables_;
public:
    /* construction */
    
    /// @param -3 means not (Variable 3), etc. 
    void addVariableParity(int i);
    
    /* accessor functions */

    typedef Variables_::const_iterator VariableConstIterator;

    VariableConstIterator getVariableBegin() const;
    VariableConstIterator getVariableEnd() const;
    
    int getNumVariables() const;

    bool getParity(Variable v) const; 
    /// print the clause
    friend std::ostream& operator<<(std::ostream& os, const Clause& s) ;
private:
    Variables_ variables_;
};

class Problem {
    /// VarToClauseMap_ contains a map from Variable to Clauses.
    /// Variable > 0, i.e., parity information is removed from the Variable. 
    typedef std::multimap<Variable, Clause*> VarToClauseMap_; 
    typedef std::vector<Clause*> ClauseContainer; 
public:
    /* construction */
    
    ~Problem();

    /// add a new clause allocated by "new"
    void addClause(Clause* c);
    
    /* accessors */

    typedef VarToClauseMap_::const_iterator VarToClauseMapIterator;
    typedef std::pair<VarToClauseMapIterator, VarToClauseMapIterator> VarToClauseMapIteratorPair;

    VarToClauseMapIteratorPair getClausesContaining(const Variable& v) const;

    typedef ClauseContainer::const_iterator ClauseConstIterator;
    ClauseConstIterator getClauseBegin() const;
    ClauseConstIterator getClauseEnd() const;
    
    int getNumVariables() const;
    
    /// print the clause
    friend std::ostream& operator<<(std::ostream& os, const Problem& s) ;
private:
    std::vector<Clause*> allClauses_; 
    VarToClauseMap_ varToClauseMap_;
};

class Solution {
public:
    Solution(const Problem& p);

    const Problem& getProblem() const;

    bool getParityOfVariable(Variable v) const;

    void flipVariable(Variable v);
    
    bool isSatisfied(Clause& c) const;
    
    /// get upto maxCount variables that lead to unsatisfaction of clause c
    std::set<Variable> computeUnsatisfiedVariables(Clause& c, int maxCount = INT_MAX) const;
    
    /// print the solution
    friend std::ostream& operator<<(std::ostream& os, const Solution& s);
private:
    std::vector<bool> parity_; //< Variable i stored at index (i-1)
    const Problem& problem_;
};

#endif
